COMMENT ⊗   VALID 00003 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002		The objective of your CS206 term project is fine - to give
C00009 00003
C00010 ENDMK
C⊗;
	The objective of your CS206 term project is fine - to give
representation indpendent sets of functions and predicates on graphs, to
axiomatize them, and to use them to prove properties of programs operating
on graphs.  You should mention that if the primitives are programmed in
LISP or some other language, it becomes necessary to prove that the
axioms for the primitives are satisfied the programs that represent them.

	However, it seems to me that you haven't described your concepts
accurately and haven't fully axiomatized their properties in first order
logic (or any other kind).  You would have been able to debug your ideas
had you tried to express your axioms in FOL or Ketonen's EKL, and persuade
the computer to accept some proofs.

	The first problem concerns graphs.  Your axioms don't deal with
graphs by themselves but with entities that might be called %2marked
graphs%1, a graph with a distinguished subset of the vertices.  This
is probably a good idea, but your exposition should make it explicit.

	%2edges[g,v]%1 is ok as a function, but the name is strange, since
its value is a list of vertices rather than a list of edges.  In fact you
deviate from the ideas announced in the first paragraphs by not using the
edges themselves as objects at all.  This may be ok for the applications
you give, but axiomatizing operations that change graphs may work better
the edges are explicitly mentioned objects.

	%2mark-visited[g,v]%1 isn't a function or predicate as it stands unless you
use marked graphs.  In this case,
%2g'_=_mark-visited[g,v]%1 is obtained from the marked graph ⊗g by marking
the vertex ⊗v.  ⊗edges[g,v] isn't still works.

	Presumably we need the axiom

	%2edges[mark-visited[g,v],v] = edges[g,v]%1.

⊗is-visited[g,v] is then ok for marked graphs.
⊗next-unvisited[g] is ok for marked graphs, assuming nil can't be a node.
%2g'_=_initialize[g]%1 is presumably the unmarked version of the marked
graph ⊗g.  ⊗all-visited[g] is ok.

	There is a problem about quantification over vertices.  You use
it as though it were quantification over the vertices of a fixed graph -
or rather whatever graph you happen to be working with.  This isn't
correct if you ever consider sentences that involve more than one
graph.  The correct alternative
is to suppose that there is a large enough supply of vertices, and
a predicate ⊗in(v,g) asserting that vertex ⊗v is in graph ⊗g. 
My schema may suffer from some of the same problems.

You also need an axiom asserting

	%2∀v.in[v,g] ⊃ ∀v1.(v1 ε edges[g,v] ⊃ in[v1,g])%1.

	%2all-visited[g] ⊃ nextunvisited[g] = nil%1

is ok.

	%2all-visited[g] ⊃ ∀v.(in[v,g] ⊃ isvisited[v,g])%1

is the form this has to take unless you want to use ⊗isvisited[v,g] in
subsequent formulas as a function expression rather than as a truth
value.  You use it as a truth value in your subsequent schema.

Again we need

	%2∀v.¬isvisited[initialize[g],v]%1.

[Your first schema is true but it isn't simply a generalization of
mine to allowing nodes of higher degree, because it doesn't involve
any use of ⊗edges[g,v].  The schema is correct, but it seems to me
that it won't be very usable, because it won't be easy to prove
¬(xεu ∧ P[g, x.u] ⊃ P[g, u]) in when the successive vertices in u
are not required to be connected.
The second version of the schema has the same objections].

I have now convinced myself that the above objections to the usefulness
of your schemas are mistaken.  It is better actually to use the
number of unvisited nodes as a rank, as you suggest, and not
use ⊗edges in the schema.  In fact, I have been gradually been
convincing myself over the last year, that all special induction
schemas are inferior to using a rank that is incorporated in the
axioms.

In describing your first representation, you say a list of visited
nodes is maintained, but your formulas don't really provide for it.
The straightforward thing is to represent a marked graph by
the ⊗cons of a list of lists and the list of visited nodes.  Then

	%2edges[g,v] = qd assoc[v, qa g]%1

	%2mark-visited[g,v] = qa g . [v . qd g]%1,

etc.

	However, it seems to me that you have confused the mathematical
notions of function and predicate with the loose usage of these terms
in programming.  It doesn't seem that your two schemas are meaningful,
although the first might be repairable, but I don't see how even to
repair the second.